ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da), L:(event-info(ds;da) List).
(ecl-halt(ds;da;x)(0,L))
 (isl(ecl-halt-kind(x)))
 ((last(L).1) = outl(ecl-halt-kind(x))  Knd) 

latex

Definitions	x(s), T, x. t(x), i <z j, b, i z j, nth_tl(n;as), hd(l), Y, ||as||, l[i], S  T, A c B, let x,y,z = a in t(x;y;z), as @ bs, Valtype(da;k), Top, , A  B, , False, True, if b then t else f fi , ff, tt, null(as), A, P  Q, x:A. B(x), last(L), t.1, t  T, b, event-info(ds;da), Knd, P  Q, x:A. B(x), P & Q, P  Q
Lemmas	outl wf, Kind-deq wf, Id wf, IdLnk wf, fpf wf, deq wf, true wf, squash wf, fpf-cap wf, ma-valtype wf, null wf3, assert wf, not wf, top wf, last append, false wf, le wf, ecl-halt-nil, last wf